(* $Id: PFOLEncoding.mli 70 2007-10-16 10:05:31Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

(** FIXME *)
exception ErrorWhenEncode of XCoreSyntax.lformula

(** FIXME *)
val bind_logic_value :
  Position.t ->
  PFOLEnv.env ->
  XCoreSyntax.id ->
  XCoreSyntax.formula_type_scheme ->
  PFOLEnv.env * PFOLSyntax.value_identifier

(** FIXME *)
val encode_binding :
  Position.t ->
  PFOLEnv.env * PFOLSyntax.Var.AtomSet.t ->
  XCoreSyntax.id * XCoreSyntax.formula_type ->
  (PFOLEnv.env * PFOLSyntax.Var.AtomSet.t) *
  (PFOLSyntax.value_identifier * PFOLSyntax.term_type)

(** FIXME *)
val encode_bindings :
  Position.t ->
  PFOLEnv.env * PFOLSyntax.Var.AtomSet.t ->
  (XCoreSyntax.id * XCoreSyntax.formula_type) list ->
  (PFOLEnv.env * PFOLSyntax.Var.AtomSet.t) *
  (PFOLSyntax.value_identifier * PFOLSyntax.term_type) list

(** FIXME *)
val convert_fprimitive :
  XCoreSyntax.formula_primitive -> PFOLSyntax.binop

(** FIXME *)
val encode_formula_as_term :
  Position.position ->
  PFOLSyntax.Var.AtomSet.t ->
  PFOLEnv.env ->
  XCoreSyntax.lformula -> PFOLEnv.env * PFOLSyntax.term

(** FIXME *)
val convert_primitive :
  XCoreSyntax.formula_primitive -> PFOLSyntax.primitive

(** FIXME *)
val encode_formulae_as_terms :
  Position.position ->
  PFOLEnv.env ->
  PFOLSyntax.Var.AtomSet.t ->
  XCoreSyntax.lformula list -> PFOLEnv.env * PFOLSyntax.term list

(** FIXME *)
val encode_fbinding :
  Position.position ->
  PFOLSyntax.Var.AtomSet.t * PFOLEnv.env ->
  XCoreSyntax.fbinding ->
  (PFOLSyntax.Var.AtomSet.t * PFOLEnv.env) * PFOLSyntax.binding

(** FIXME *)
val encode_fbindings :
  Position.position ->
  PFOLEnv.env ->
  XCoreSyntax.fbindings ->
  (PFOLSyntax.Var.AtomSet.t * PFOLEnv.env) * PFOLSyntax.bindings

(** FIXME *)
val remove_locals : PFOLSyntax.Var.AtomSet.t -> PFOLEnv.env -> PFOLEnv.env

(** FIXME *)
val encode_pre_eq :
  Position.position ->
  PFOLSyntax.Var.AtomSet.t ->
  PFOLEnv.env ->
  XCoreSyntax.lformula ->
  XCoreSyntax.var -> PFOLEnv.env * PFOLSyntax.predicate

(** FIXME *)
val encode_post_eq :
  Position.position ->
  PFOLSyntax.Var.AtomSet.t ->
  PFOLEnv.env ->
  XCoreSyntax.lformula ->
  XCoreSyntax.var -> PFOLEnv.env * PFOLSyntax.predicate

(** FIXME *)
val encode_eq :
  Position.position ->
  PFOLSyntax.Var.AtomSet.t ->
  PFOLEnv.env ->
  XCoreSyntax.lformula ->
  XCoreSyntax.lformula -> PFOLEnv.env * PFOLSyntax.predicate

(** FIXME *)
val encode_single_eq :
  Position.position ->
  PFOLSyntax.Var.AtomSet.t ->
  PFOLEnv.env ->
  XCoreSyntax.lformula ->
  XCoreSyntax.lformula -> PFOLEnv.env * PFOLSyntax.predicate

(** FIXME *)
val encode_formula_as_predicate :
  Position.position ->
  PFOLEnv.env -> XCoreSyntax.lformula -> PFOLEnv.env * PFOLSyntax.predicate
